Nuprl Lemma : lnk-decl_wf
11,40
postcript
pdf
l
:IdLnk,
dt
:fpf(Id;
tg
.Type). lnk-decl(
l
;
dt
)
fpf(Knd;
k
.Type)
latex
Definitions
IdLnk
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
id-deq
,
outl(
x
)
,
t
.2
,
fpf-ap(
f
;
eq
;
x
)
,
Knd
,
x
.
t
(
x
)
,
t
.1
,
rcv(
l
,
tg
)
,
map(
f
;
as
)
,
lnk-decl(
l
;
dt
)
,
fpf(
A
;
a
.
B
(
a
))
,
guard(
T
)
,
P
Q
,
sq_type(
T
)
,
prop{i:l}
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
pi2
wf
,
member
map
,
Knd
sq
,
map
wf
,
rcv
wf
,
pi1
wf
,
Knd
wf
,
l
member
wf
,
Id
wf
,
IdLnk
wf
origin
l:IdLnk, dt:fpf(Id; tg.Type). lnk-decl(l; dt) 
fpf(Knd; k.Type) l:IdLnk, dt:fpf(Id; tg.Type). lnk-decl(l; dt) fpf(Knd; k.Type) Tx:A. B(x) l)
x. t(x)
Q
Q
x:A. B(x)
Q